E,X1,X2:Type, info:(E((:Id  X1) + (:(:IdLnk  E)  X2))), pred?:(E(?E)),
p:(e:E, l:IdLnk.
p:(e':E
p:((e'':E. 
p:((rcv?(e''))
p:( (sender(e'') = e)
p:( (link(e'') = l)
p:( (((e'' = e')  e'' < e')  (loc(e') = destination(l)  Id)))),
e:E, l:IdLnk.
guard((e'':E. 
guard((rcv?(e''))
guard( (sender(e'') = e)
guard( (link(e'') = l)
guard( (((e'' = sends-bound(p; e; l))  e'' < sends-bound(p; e; l))
guard(  (loc(sends-bound(p; e; l)) = destination(l)  Id)))) 

latex

Definitions	x:A. B(x), x:A. B(x), P  Q, P  Q, P  Q, guard(T), sends-bound(p; e; l), t.1, t  T, prop{i:l}
Lemmas	assert wf, rcv? wf, sender wf, IdLnk wf, link wf, cless wf, Id wf, loc wf, ldst wf, unit wf